Problem:
 a__c() -> a__f(g(c()))
 a__f(g(X)) -> g(X)
 mark(c()) -> a__c()
 mark(f(X)) -> a__f(X)
 mark(g(X)) -> g(X)
 a__c() -> c()
 a__f(X) -> f(X)

Proof:
 Bounds Processor:
  bound: 3
  enrichment: match
  automaton:
   final states: {6,5,4}
   transitions:
    f1(45) -> 46*
    f1(47) -> 48*
    f1(39) -> 40*
    c1() -> 7*
    g1(15) -> 16*
    g1(17) -> 18*
    g1(7) -> 8*
    g1(23) -> 24*
    a__f1(37) -> 38*
    a__f1(29) -> 30*
    a__f1(31) -> 32*
    a__f1(8) -> 9*
    a__c1() -> 25*
    f2(75) -> 76*
    f2(67) -> 68*
    f2(69) -> 70*
    f2(61) -> 62*
    c2() -> 54*
    a__c0() -> 4*
    g2(59) -> 60*
    g2(54) -> 55*
    a__f0(2) -> 5*
    a__f0(1) -> 5*
    a__f0(3) -> 5*
    a__f2(55) -> 56*
    g0(2) -> 1*
    g0(1) -> 1*
    g0(3) -> 1*
    f3(83) -> 84*
    c0() -> 2*
    g3(79) -> 80*
    mark0(2) -> 6*
    mark0(1) -> 6*
    mark0(3) -> 6*
    f0(2) -> 3*
    f0(1) -> 3*
    f0(3) -> 3*
    1 -> 45,31,17
    2 -> 47,29,15
    3 -> 39,37,23
    7 -> 59,4
    8 -> 75*
    9 -> 4*
    16 -> 32,6,5
    18 -> 32,6,5
    24 -> 32,6,5
    25 -> 6*
    29 -> 61*
    30 -> 6*
    31 -> 67*
    32 -> 6*
    37 -> 69*
    38 -> 6*
    40 -> 5*
    46 -> 5*
    48 -> 5*
    54 -> 79,25,6
    55 -> 83*
    56 -> 25,6
    60 -> 9,4
    62 -> 30*
    68 -> 32,6
    70 -> 38,6
    76 -> 9,4
    80 -> 56,25
    84 -> 56,25
  problem:
   
  Qed